es:event_system{i:l}, e1,e2:es-E(es).
es-le(es; e1; e2)  sqequal(last(es-hist{i:l}(es;e1;e2)); es-info(es;e2)) 

latex

Definitions	b, t  T, top, x:A. B(x), loc(e), Id, es-E(es), subtype(S; T), [e, e'], P  Q, es-hist{i:l}(es;e1;e2), event_system{i:l}, es-le(es; e; e'), False, A, P  Q, es-locl(es; e; e'), P  Q, P  Q, prop{i:l}, null(as)
Lemmas	es-interval-last, assert of null, assert wf, null wf3, not functionality wrt iff, es-interval-nil, es-interval wf, es-locl wf, es-le-not-locl, es-le-loc, es-loc-pred, es-le wf, event system wf, last-map, es-interval wf2, top wf, es-E wf, Id wf, es-loc wf